/*
 * somETIMES: linEar Temporal logIc MachinE for Scala (http://code.google.com/p/sometimes/)
 *
 * Copyright (C) 2010 Karolis Kleiza
 *
 * This program is free software; you can redistribute it 
 * and/or modify it under the terms of the GNU General Public License 
 * as published by the Free Software Foundation; either version 3 
 * of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful, 
 * but WITHOUT ANY WARRANTY; without even the implied warranty of 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 
 * GNU General Public License for more details.
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, see <http://www.gnu.org/licenses/>.
 */

package de.kleiza.utilities.sometimes
import scala.collection.Iterator

abstract case class LTLExp extends Iterable[LTLExp] {

  def hasTemporalOps: Boolean
  def makeStep: LTLExp

  def evaluate: LTLExp
  def evaluateOnlyPreds: LTLExp

  def iterator: Iterator[LTLExp] = ({ a: LTLExp =>
    val iter = new Iterator[LTLExp] {
      var exp: LTLExp = a next
      def next = {
        exp = exp.makeStep.evaluate
        exp
      }
      def hasNext() = { !exp.isInstanceOf[Result] }
    }
    iter
  })(this)

  def deepCopy: LTLExp

  def &&(that: LTLExp): LTLExp = {
    val ret = that match {
      case b: Result => that && this
      case _ => AndOp(this, that)
    }
    ret
  }

  def ||(that: LTLExp): LTLExp = {
    val ret = that match {
      case b: Result => that || this
      case _ => OrOp(this, that)
    }
    ret
  }

  def unary_!(): LTLExp = {
    NotOp(this)
  }

  def until(that: LTLExp): LTLExp = {
    UntilOp(this, that)
  }

  def calls(func: Boolean => Unit) = {
    Calls(this, func)
  }

  def sync(): LTLExp = {
    Sync(this)
  }

  def next(): LTLExp = {
    NextOp(this)
  }

  def next(steps: Int): LTLExp = {
    NextOp(this, steps)
  }

  //not fundamental operators
  def fin(): LTLExp = {
    True until this
  }

  def global(): LTLExp = {
    False release this
  }

  def release(that: LTLExp): LTLExp = {
    !(!this until !that)
  }
}

case class Calls(var exp: LTLExp, func: Boolean => Unit) extends LTLExp {

  override def evaluateOnlyPreds = { exp = exp.evaluateOnlyPreds; this }

  override def hasTemporalOps = { exp.hasTemporalOps }

  override def toString = { "(" + exp + " calls " + func + ")" }

  override def deepCopy = {
    copy(exp = exp.deepCopy)
  }

  override def evaluate: LTLExp = {
    val expEval = exp.evaluate match {
      case r: Result => func(r.result); r
      case r => r
    }
    expEval
  }

  def makeStep = {
    exp = exp.makeStep
    this
  }
}

case class Sync(var exp: LTLExp) extends LTLExp {
  override def evaluateOnlyPreds = { exp = exp.evaluateOnlyPreds; this }

  //TODO: check if correct
  override def hasTemporalOps = { exp.hasTemporalOps }

  override def toString = { "Sync(" + exp + ")" }

  override def deepCopy = {
    copy(exp = exp.deepCopy)
  }

  override def evaluate: LTLExp = {
    val expEval = if (!exp.hasTemporalOps) { exp.evaluate } else { evaluateOnlyPreds }
    expEval
  }

  def makeStep = {
    exp = exp.makeStep
    this
  }
}

abstract case class BooleanExp extends LTLExp {

}

abstract case class TemporalExp extends LTLExp {
  override def hasTemporalOps = { true }
  override def evaluateOnlyPreds = {this}
  override def evaluate: LTLExp = {
    this
  }
}

case class AndOp(var left: LTLExp, var right: LTLExp) extends BooleanExp {
  override def hasTemporalOps = { left.hasTemporalOps || right.hasTemporalOps }
  override def evaluateOnlyPreds = {
    left = left.evaluateOnlyPreds; right = right.evaluateOnlyPreds
    this
  }

  override def toString = { "(" + left + " && " + right + ")" }

  override def deepCopy = {
    copy(left.deepCopy, right.deepCopy)
  }
  override def evaluate: LTLExp = {
    left.evaluate && right.evaluate
  }

  override def makeStep: LTLExp = {
    left = left.makeStep
    right = right.makeStep
    this
  }
}

case class OrOp(var left: LTLExp, var right: LTLExp) extends BooleanExp {
  override def evaluateOnlyPreds = {
    left = left.evaluateOnlyPreds; right = right.evaluateOnlyPreds; this
  }

  override def hasTemporalOps = { left.hasTemporalOps || right.hasTemporalOps }

  override def toString = { "(" + left + " || " + right + ")" }

  override def deepCopy = {
    copy(left.deepCopy, right.deepCopy)
  }
  override def evaluate: LTLExp = {
    left.evaluate || right.evaluate
  }

  override def makeStep: LTLExp = {
    left = left.makeStep
    right = right.makeStep
    this
  }
}

case class NotOp(var exp: LTLExp) extends BooleanExp {
  override def evaluateOnlyPreds = { exp = exp.evaluateOnlyPreds;this }
  override def hasTemporalOps = { exp.hasTemporalOps }

  override def toString = { " !" + exp }

  override def deepCopy = {
    copy(exp = exp.deepCopy)
  }
  override def evaluate: LTLExp = {
    !(exp.evaluate)
  }
  override def makeStep: LTLExp = {
    exp = exp.makeStep
    this
  }
}

abstract case class Predicate extends BooleanExp {
  override def evaluateOnlyPreds = { evaluate }
  override def hasTemporalOps = { false }

  override def toString = { "P(function)" }
  override def makeStep: LTLExp = {
    this
  }
}

case class Pred(pred: Function0[Boolean]) extends Predicate {

  override def deepCopy = {
    copy()
  }

  override def evaluate: LTLExp = {
    Result(pred())
  }
}

case class AnnoPred[A](pred: Function0[Tuple2[Boolean, A]]) extends Predicate {

  override def deepCopy = {
    copy()
  }

  override def evaluate: LTLExp = {
    val (ret, anno) = pred()
    AnnotatedResult[A](ret, anno)
  }
}

case class NextOp(exp: LTLExp, var steps: Int = 1) extends TemporalExp {

  override def toString = { "next" + steps + "(" + exp + ")" }

  override def deepCopy = {
    copy(exp = exp.deepCopy)
  }
  override def makeStep = {
    val ret = if (steps <= 1) exp else { steps -= 1; this }
    ret
  }
}

case class UntilOp(left: LTLExp, right: LTLExp) extends TemporalExp {
 
  override def toString = { "(" + left + " until " + right + ")" }
  override def deepCopy = {
    copy(left.deepCopy, right.deepCopy)
  }

  override def evaluate = {
    val copy = deepCopy
    val ret = right.evaluate || (left.evaluate && (copy next))
    ret
  }

  override def makeStep = {
    this
  }
}

case class Result(var result: Boolean) extends BooleanExp {
  override def evaluateOnlyPreds = { this }
  override def hasTemporalOps = { false }
  override def toString = { result.toString }
  override def deepCopy = {
    copy()
  }

  override def evaluate: LTLExp = {
    this
  }

  def makeStep = {
    this
  }

  override def &&(that: LTLExp): LTLExp = {
    val ret: LTLExp = result match {
      case true => that
      case false => this
    }
    ret
  }
  override def ||(that: LTLExp): LTLExp = {
    val ret: LTLExp = result match {
      case true => this
      case false => that
    }
    ret
  }
  override def unary_!(): LTLExp = {
    result = !result
    this
  }
}

case class AnnotatedResult[A](result2: Boolean, anno: A) extends Result(result2) {
  override def toString = { "(" + result + "," + anno + ")" }

  override def makeStep = {
    this
  }

}

object True extends Result(true)

object False extends Result(false)
